Design verification is the process of determining whether an integrated circuit, board, or system-level architecture, exactly implements the requirements defined by the specification of the architecture for that device. Design verification for a device under testing (DUT) may be performed on the actual device, or on a simulation model of the device. For the purposes of explanation only and without intending to be limiting in any way, the following discussion centers upon testing which is performed on simulation models of the device.
As designs for different types of devices and device architectures become more complex, the likelihood of design errors increases. However, design verification also becomes more difficult and time consuming, as the simulation models of the design of the device also become more complex to prepare and to test
The problem of design verification is compounded by the lack of widely generalizable tools which are useful for the verification and testing of a wide variety of devices and device architectures. Typical background art verification methods have often been restricted to a particular device having a specific design, such that the steps of preparing and implementing such verification methods for the simulation model must be performed for each new device.
The process of verifying a design through a simulation model of the device is aided by the availability of hardware description languages such as Verilog and VHDL. These languages are designed to describe hardware at higher levels of abstraction than gates or transistors. The resultant simulated model of the device can receive input stimuli in the form of test vectors, which arc a string of binary digits applied to the input of a circuit. The simulated model then produces results, which are checked against the expected results for the particular design of the device. However, these languages are typically not designed for actual verification. Therefore, the verification engineer must write additional programming code in order to interface with the models described by these hardware description languages in order to perform design verification of the device.
Examples of testing environments include static and dynamic testing environments. A static testing environment drives pre-computed test vectors into the simulation model of the DUT and/or examines the results after operation of the simulation model. In addition, if the static testing environment is used to examine the results which are output from the simulation model, then errors in the test are not detected until after the test is finished. As a result, the internal state of the device at the point of error may not be determinable, requiring the simulation to be operated again in order to determine such internal states. This procedure consumes simulation cycles, and can require the expenditure of considerable time, especially during long tests.
A more useful and efficient type of testing is a dynamic testing environment. For this type of environment, a set of programming instructions is written to generate the test vectors in concurrence with the simulation of the model of the DUT and while potentially being controlled by the state feedback of the simulated device. This procedure enables directed random generation to be performed and to be sensitive to effects uncovered during the test itself on the state of the simulation model of the device. Thus, dynamic test generation clearly has many advantages for design verification.
Within the area of testing environments, both static and dynamic testing environments can be implemented only with fixed-vector or pre-generation input. However, a more powerful and more sophisticated implementation uses test generation to produce the environment.
One example of such a test generator is disclosed in U.S. Pat. No. 6,182,258, filed on Feb. 6, 1998, incorporated by reference as if fully set forth herein. This test generation procedure interacts with, and sits as a higher level over, such hardware description languages as Verilog and VHDL. The test generation procedure is written in a hardware-oriented verification specific object-oriented programming language. This language is used to write various tests, which are then used to automatically create a device verification test by a test generator module. A wide variety of design environments can be tested and verified with this language. Thus, the disclosed procedure is generalizable, yet is also simple to program and to debug by the engineer.
This language features a number of elements such as structs for more richly and efficiently describing the design of the device to be simulated by the model. Unfortunately, the disclosed language and resultant test generation environment does not include features for testing the state of the device over time. Such testing is performed by sampling the values for various variables at different times, either according to some triggering event or at predetermined times, and is termed “temporal coverage”. Temporal coverage is a collection of coverage information based on the occurrence of some pattern in time, with the pattern itself being defined according to a temporal language. Temporal coverage differs from automatic coverage, which is triggered by the appearance of a line of code or other static event, in that temporal coverage is driven by the occurrence of events in time. Temporal coverage enables the behavior of the device to be monitored over time during the testing period, particularly since a circuit or other DUT cannot be exhaustively simulated, such that all relevant states are tested. Analysis of the coverage enables the designer to determine which states of the device require further testing. Such analysis can be facilitated with abstract state machines.
Various temporal languages are known in the background art, yet the construction and evaluation of expressions in such languages for the purpose of temporal coverage for design verification has so far proven to be highly limited. In particular, there is a requirement in design verification for describing and monitoring the behavior of concurrent systems such as digital hardware or communication protocols. Currently, such behavior is commonly characterized in the background art (as discussed in standard texts on the subject such as that of Emerson A., in The Handbook of Theoretical Computer Science, Elsevier, 1990) according to sequences of configurations of the system under consideration, or according to sequences of events occurring within the system. However, a more useful solution to this problem would enable both methods to be used when specifying behavior in temporal expressions.
The task of evaluating temporal expressions in a programming system is more complicated than that of evaluating logical or arithmetic expressions since a sequence of states, or snapshots of the program memory, must be considered, rather than a single state. Temporal expression evaluation commences at some point during program execution, and continues over a number of cycles of a clock defined by the program until the expression either succeeds or it fails. Success indicates that the preceding sequence of program states complies with, or satisfies, the mathematical definition of the temporal expression; failure indicates the converse.
Typically, the evaluation of a temporal expression is performed by using an abstract state machine, or automaton. These automata preserve only the minimum necessary information at each state, and in the transitions between states, rather than a complete snapshot of the program memory. Programming languages such as C or Verilog provide mechanisms for constructing automata that may represent temporal behavior by explicitly enumerating their states and the transitions between states. Other languages such as those based on the temporal logics CTL and LTL allow one to specify temporal behavior in a non-procedural declarative style by writing down a formula. Temporal e is a language of this latter kind (see for example SMV—“Symbolic Model Checking” Ken McMillan, Kluwer Academic Press 1993; Sugar—“Rule Base: an industry oriented formal verification tool” I. Beer et al. Proceedings DAC, ACM June 1996).
Since a temporal expression, or formula, represents the behavior implicitly it is necessary to devise a mechanism to recognize or implement that behavior. For temporal logics like CTL and LTL the common approach is to construct an automaton from the text of the formula via a procedure known as a tableau construction—so called because the tree like structure the procedure builds is known as a proof tableau in formal logic. For LTL and CTL the construction always gives rise to a finite automaton, but the details vary considerably because the procedures depend intimately on the mathematical semantics of the language concerned. For references to the background art see for example the work of Clarke et al. in Proceedings of Computer-Aided Verification, Springer-Verlag, 1994.
While LTL and CTL are targeted at formal verification, the e temporal language is primarily directed at simulation. While still applicable to formal verification, this language has proven to be easier and more intuitive to use, particularly for simulation, but still lacks a construction scheme.